Nuprl Lemma : band_commutes
4,23
postcript
pdf
a
,
b
:
. (
a
b
) = (
b
a
)
latex
Definitions
x
:
A
.
B
(
x
)
,
,
Unit
,
t
T
,
true
,
false
Lemmas
bfalse
wf
,
btrue
wf
,
bool
wf
origin
a, b:
. (a 
b) = (b a) 
a, b:. (a b) = (b a) x:A. B(x) T